$\forall$$g$:OCMon, $a$, $b$:$\mid$$g$$\mid$. Dec($a$ $<$ $b$)